#|
conway-topo: An ACL2 implementation of Conway's Game of Life on several topologies
Copyright (C) 2007 Vanessa Cheney, Jennifer Foley, Gerardo Gonzalez and John O'Hare

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
|#

(include-book "avl" :dir:system)

#|
Returns a new World object with the node added to the input 
World's alive cells tree if the node does not already exist 
in the given world.

@param nodeId The node to add to the passed in World object's alive cells tree
@param theWorld The World object to alter
@return A new World object that is identical to the input theWorld object except
    with a node possibly added to the alive cells tree
|#
(defun addNode (nodeId theWorld)
  t)

#|
Returns a new World object with the specified node deleted from the input 
World's alive cells tree if the note exists in the given world

@param nodeId The node to delete from the passed in World object's alive cells tree
@param theWorld The World object to alter
@return A new World object that is identical to the input theWorld object except
    with a node possibly deleted from the alive cells tree
|#
(defun deleteNode (nodeId theWorld)
  t)

#|
Looks for a node within the alive cells tree of the given World object

@param nodeId The node to search for within the input World object
@param theWorld The world object whose alive cells tree will be searched
@return t if the node was found, or nil if it was not
|#
(defun search (nodeId theWorld)
  t)

#|
Returns the data at the root of the left subtree of the given binary tree

@param tree The binary tree to return the data from
@return Whatever data is at the root of the left subtree of the input tree, 
    or nil if there is not a left subtree or there is no data at its root
|#
(defun leftChild (tree)
  t)

#|
Returns the data at the root of the right subtree of the given binary tree

@param tree The binary tree to return the data from
@return Whatever data is at the root of the right subtree of the input tree, 
    or nil if there is not a right subtree or there is no data at its root
|#
(defun rightChild (tree)
  t)

#|
Returns the left subtree of the given tree

@param tree The binary tree to return the left subtree from
@return Whatever data is at the root of the left subtree of the input tree, 
    or nil if there is not a left subtree
|#
(defun leftSubtree (tree)
  t)

#|
Returns the right subtree of the given tree

@param tree The binary tree to return the right subtree from
@return Whatever data is at the root of the right subtree of the input tree, 
    or nil if there is not a right subtree
|#
(defun rightSubtree (tree)
  t)

#|
Returns t if the specified node is alive and nil if it is not 
or if the nodeId is invalid

@param nodeId The id of the node to check
@param theWorld The World object whose alive nodes tree will be checked for 
    the given node
@return t if the node is alive, and nil if it is not or the nodeId is invalid
|#
(defun isAlive (nodeId theWorld)
  (search nodeId theWorld))

#|
Returns the number of direct neighbors of the given node that are alive in the 
given world object

@param nodeId 
@param theWorld 
@return The number of neighbors of node # nodeId that are alive in theWorld
|#
(defun numNeighborsAlive (nodeId tree)
  t)

#|
Removes duplicates from a given sorted list

@param list A sorted true list of rational numbers
@return The same list, but with duplicate entries removed
|#
(defun removeDups (list)
  (if (consp list)
      (if (consp (cdr list))
          (if (= (car list)
                 (cadr list))
              (removeDups (cdr list))
              (cons (car list) (removeDups (cdr list))))
          list)
      nil))

(defstructure World
  (tree (:assert (isTree tree)))
  (height (:assert (natp height)))
  (width (:assert (natp width)))
  (topology (:assert (symbolp topology))))

(defconst *CURRENTWORLD* (World nil 5 20 'rectangle))

(defun aboveNeighbor (topology cell w h)
  (if (= (Coord-cellY cell) h)
      (case topology
        ('regular nil)
        ('moebius nil)
        ('cylindar nil)
        ('torus (Coord (Coord-cellX cell) 0))
        ('klein (Coord (- (Coord-cellX cell) w) 0))
        (otherwise nil))
      (Coord (Coord-cellX cell) (+ (Coord-cellY cell) 1))))

(defun belowNeighbor (topology cell w h)
  (if (= (Coord-cellY cell) 0)
      (case topology
        ('regular nil)
        ('moebius nil)
        ('cylindar nil)
        ('torus (Coord (Coord-cellX cell) h))
        ('klein (Coord (- (Coord-cellX cell) w) h))
        (otherwise nil))
      (Coord (Coord-cellX cell) (- (Coord-cellY cell) 1))))

(defun leftNeighbor (topology cell w h)
  (if (= (Coord-cellX cell) 0)
      (case topology
        ('regular nil)
        ('moebius (Coord w (- (Coord-cellY cell) h)))
        ('cylindar (Coord w (Coord-cellY cell)))
        ('torus (Coord w (Coord-cellY cell)))
        ('klein (Coord w (- (Coord-cellY cell) h)))
        (otherwise nil))
      (Coord (- (Coord-cellX cell) 1) (Coord-cellY cell))))

(defun rightNeighbor (topology cell w h)
  (if (= (Coord-cellX cell) w)
      (case topology
        ('regular nil)
        ('moebius (Coord 0 (- (Coord-cellY cell) h)))
        ('cylindar (Coord 0 (Coord-cellY cell)))
        ('torus (Coord 0 (Coord-cellY cell)))
        ('klein (Coord 0 (- (Coord-cellY cell) h)))
        (otherwise nil))
      (Coord (+ (Coord-cellX cell) 1) (Coord-cellY cell))))

(defun aboveLeftNeighbor (topology cell w h)
  (if (or (not (leftNeighbor topology cell w h))
          (not (aboveNeighbor topology cell w h)))
      nil
      (Coord (Coord-cellX (leftNeighbor topology cell w h))
             (Coord-cellY (aboveNeighbor topology cell w h)))))
      
(defun aboveRightNeighbor (topology cell w h)
  (if (or (not (rightNeighbor topology cell w h))
          (not (aboveNeighbor topology cell w h)))
      nil
      (Coord (Coord-cellX (rightNeighbor topology cell w h))
             (Coord-cellY (aboveNeighbor topology cell w h)))))

(defun belowLeftNeighbor (topology cell w h)
  (if (or (not (leftNeighbor topology cell w h))
          (not (belowNeighbor topology cell w h)))
      nil
      (Coord (Coord-cellX (leftNeighbor topology cell w h))
             (Coord-cellY (belowNeighbor topology cell w h)))))

(defun belowRightNeighbor (topology cell w h)
  (if (or (not (rightNeighbor topology cell w h))
          (not (belowNeighbor topology cell w h)))
      nil
      (Coord (Coord-cellX (rightNeighbor topology cell w h))
             (Coord-cellY (belowNeighbor topology cell w h)))))

(defun getNeighbors (topology cell w h)
  (list*
   (aboveNeighbor topology cell w h)
   (belowNeighbor topology cell w h)
   (leftNeighbor topology cell w h)
   (rightNeighbor topology cell w h)
   (belowLeftNeighbor topology cell w h)
   (belowRightNeighbor topology cell w h)
   (aboveLeftNeighbor topology cell w h)
   (aboveRightNeighbor topology cell w h)))

(defun aliveMembers (topology list w h tree)
  (if (consp list)
      (if (isAlive (car list) tree)
          (cons (car list) (aliveMembers topology (cdr list) w h tree))
          (aliveMembers topology (cdr list) w h tree))
      nil))

(defun aliveNeighbors (topology cell w h tree)
  (aliveMembers topology (getNeighbors topology cell w h) w h tree))

(defun numNeighborsAlive (cell topology w h tree)
  (count (aliveNeighbors topology cell w h tree)))

(defun allNeighbors (list topology w h)
  (if (consp list)
      (list* (getNeighbors topology (car list) w h)
             (allNeighbors (cdr list) topology w h))
      nil))

(defun getNodesToCheck (tree topology w h)
  (list* (avl-flatten tree)
         (allNeighbors (avl-flatten tree) topology w h)))

(defun isAliveNextRound (cell tree topology w h)
  (let* ((numAlive (numNeighborsAlive cell topology w h tree)))
    (if (or (and (isAlive cell tree)
                 (= numAlive 2))
            (= numAlive 3))
        t
        nil)))

(defun allAliveNextRound (list tree topology w h)
  (if (consp list)
      (if (isAliveNextRound (car list) tree topology w h)
          (cons (car list) (allAliveNextRound (cdr list) tree topology w h))
          (allAliveNextRound (cdr list) tree topology w h))
      nil))

(defun putInTree (list)
  (if (consp list)
      (avl-insert (putInTree (cdr list)) (car list) t)
      (empty-tree)))

(defun gerardosNextWorld (world)
  (let* ((toCheck (getNodesToCheck (World-tree world)
                                   (World-topology world)
                                   (World-width world)
                                   (World-height world))))
    (World 
     (putInTree (allAliveNextRound toCheck 
                                   (World-tree world)
                                   (World-topology world)
                                   (World-width world)
                                   (World-height world)))
     (World-height world)
     (World-width world)
     (World-topology world))))
  



